substring
String.substring
create substring of this string consisting of bytes from (inclusive) .. to (exclusive).
Precondition
pre debug: 0 ≤ from ≤ to ≤ String.this.byte_count debug: from=to || String.is_valid_utf8_first_byte utf8[from] debug: from=to || !String.is_multi_byte_start_byte utf8[to-1]
Postcondition
post debug 10 : result.codepoints_and_errors ∀ x->x.ok
0.095dev (GIT hash 91033acfd0b07a6e4c620ce81166841b8de33a6f)